T:Type, L_1, L_2:(T List). L_1  L_2  L_1  L_2 

latex

Definitions	suptype(S; T), S  T, , i  j < k, t  T, P & Q, {i..j}, x:A. B(x), L1  L2, P  Q, x:A. B(x), , False, A, P  Q, A  B, A c B
Lemmas	iseg wf, select wf, increasing wf, non neg length, id increasing, int seg wf, le wf, length wf1, iseg select, iseg length